Hold 0114's two acts, and put the local half of a sign-out before the request - #263

The issue this belongs to

#114. This does not close it, and the reason is at the end.

What changed

src/session/sign_out.rs holds the part of 0114 a type, a table and a pair of
counts settle.

The order is a type. TellingTheServer is produced by
LocalHalf::what_is_left_for_the_server and by nothing else, so a caller cannot
reach the request before the local half is a value it holds. LocalHalf has no
failure: the server half is the only one 0114 allows to fail, so a sign-out on a
train completes and reports that the server was not told.

what_it_takes_away is the difference between the two acts, in 0114's own list.
A sign-out drops the token and forgets the secret. Forgetting a server does both
and then removes the cache entries, the queue and the index rows for them, which
is strictly the first plus removal.

how_it_ends is the table for the four kinds of work that can be running when a
sign-out arrives, each ending in its own named state.

Removal carries what was removed and what could not be reached, and has no
success value.

LocalHalf::after_a_renewal is the other side of 0034: a refused renewal signs
the session out with the server half skipped, and it is always the plain act.

What failure it prevents

A token still in memory on a device somebody has handed over. 0114 names
that as the failure the whole act exists against, and the shape that produces it
is the local half waiting on the server half - which is what gets written,
because a request is the interesting part and the ordering is not visible at a
call site. The type is what refuses it here.

A library emptied by an ordinary evening act, or an operator's removal request
with nothing behind it. Those are the two directions of collapsing the two acts
into one button, which is what every client that was not told they differ does.

An operator told their data was removed when it was not. A success value is
what gets returned by a removal that walked what it could find, and somebody who
was told their data is gone has no reason ever to ask again.

A call abandoned inside a client's own implementation. 0115 refuses that
without exception, and a sign-out cancelling everything it can see is exactly how
it happens.

None of the four has happened here: nothing in this tree signs anything out. This
is the constraint written before the caller, which is the argument 0114 makes for
itself under "why this is written down before the code".

Evidence

Every command run at 74aa6c1d0a0f356adcb0082abd839986c94b71ed, the head being
pushed.

cargo build --locked --all-targets
Finished `dev` profile [unoptimized + debuginfo] target(s) in 3.91s

cargo test --locked 2>&1 | grep -c '^test .* ok$'
621

cargo test --locked 2>&1 | grep -c '^test result: FAILED'
0

cargo test --locked --lib session::sign_out 2>&1 | grep -E '^test result'
test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 453 filtered out; finished in 0.00s

The legs of the gate this machine can run, each by its own script and each by its
own exit code:

for s in format invariants doc-paths lint test excluded-targets targets; do
  bash .github/$s/$s.sh check >/dev/null 2>&1; echo "$s exit=$?"
done
format exit=0
invariants exit=0
doc-paths exit=0
lint exit=0
test exit=0
excluded-targets exit=0
targets exit=0

cargo clippy --all-targets -- -D warnings -D clippy::all -D clippy::pedantic -D clippy::cargo 2>&1 | grep -cE '^(error|warning)'
0

What a guard here refuses, and the proof it bites

Four violations, each applied to the working tree, run, and reverted.

A sign-out does not remove the cache. The violation is the one button:

(in what_it_takes_away, the Act::SignOut arm)
+            WhatIsTakenAway::TheCacheEntries,

cargo test --locked --lib session::sign_out 2>&1 | grep -E '^    session|^test result'
    session::sign_out::tests::a_sign_out_leaves_the_cache_and_the_queue_and_a_forget_does_not
    session::sign_out::tests::only_a_refusal_signs_out_and_it_is_never_the_stronger_act
test result: FAILED. 11 passed; 2 failed; 0 ignored; 0 measured; 453 filtered out

A call inside the client's store runs to completion. The violation is the
sign-out that cancels everything it can see:

-        WorkInFlight::ACallInsideTheClientsStore => HowItEnds::CompletesInsideTheClientsCode,
+        WorkInFlight::ACallInsideTheClientsStore => HowItEnds::CancelledAndALateAnswerDiscarded,

cargo test --locked --lib session::sign_out 2>&1 | grep -E '^    session|^test result'
    session::sign_out::tests::each_kind_of_work_in_flight_ends_in_its_own_named_state
test result: FAILED. 12 passed; 1 failed; 0 ignored; 0 measured; 453 filtered out

A forced sign-out does not tell the server. The violation drops the half of
the condition that reads why:

-            tell_the_server: !forced && !already_signed_out,
+            tell_the_server: !already_signed_out,

cargo test --locked --lib session::sign_out 2>&1 | grep -E '^    session|^test result'
    session::sign_out::tests::a_refused_renewal_signs_out_without_telling_the_server
test result: FAILED. 12 passed; 1 failed; 0 ignored; 0 measured; 453 filtered out

A failed attempt says the token may still be live. The violation is the
tidier-looking report that loses the fact an operator can act on:

-        (true, Some(false)) => WhatTheClientIsTold::TheServerWasNotToldAndTheTokenMayStillBeLive,
+        (true, Some(false)) => WhatTheClientIsTold::ThereWasNothingToTell,

cargo test --locked --lib session::sign_out 2>&1 | grep -E '^    session|^test result'
    session::sign_out::tests::a_failed_attempt_reports_that_the_token_may_still_be_live
test result: FAILED. 12 passed; 1 failed; 0 ignored; 0 measured; 453 filtered out

The order is a compile failure rather than a red line, and that is stated
plainly rather than dressed as a test result. TellingTheServer has no public
constructor and no public field, so a caller that wanted to send before
completing the local half has nothing to build. No run demonstrates that, because
the violation does not compile.

With all four restored:

cargo test --locked --lib session::sign_out 2>&1 | grep -E '^test result'
test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 453 filtered out; finished in 0.00s

What this does not cover

#114's own three conditions are untouched and this does not close it. Each
signs in against a server - two at once for the first - and nothing in this tree
signs in. The request is #27 and a core to hold a session in is #115. The reading
already on the issue about which surfaces exist and which do not is not restated
in this body.

Nothing signs anything out. No token is dropped because there is none, no
store is called because none is held, no queue is drained and no entry is
removed. This says what the acts do and performs none of it.

The set a forget removes is not computed here. 0114 makes it the entries
whose first three parts are that server, that account and that device identity,
and finding them is the index 0042 holds. Removal counts what an act reached
and what it could not, which is the half 0114 requires be reported.

Nothing here is about lanes. 0114 says cancelling by session rather than by
lane is the part that will be got wrong, and no signature in this module can
express a lane, which is the whole of what it can do about that. The unit of work
that would carry its session does not exist.

The coverage leg was not judged on this machine. Its instrumentation reads
zero lines for every area here, on this branch and on an unmodified checkout of
the default branch alike, so the number is absent rather than low.
.github/workflows/coverage.yml runs on this pull request and is what judges it.
The pinned-surface register carries the new module with its reason.

Three other legs were not run here. headless needs a program this machine
does not carry (ip: command not found), thread-detector needs a nightly
compiler this tree deliberately does not pin, and mutation is weekly rather
than a pull-request leg. None was skipped by editing anything; they were not run.

Who has read it

Nobody but me has read this change. There is no second reader on this board
tonight, and the evidence above stands in place of one rather than the question
being left open.